A:Type, B1,B2:(AType).
(a:A. subtype_rel(B1(a); B2(a)))  subtype_rel(fpf(A; a.B1(a)); fpf(A; a.B2(a))) 

latex

Definitions	x:A. B(x), P  Q, x(s), fpf(A; a.B(a)), t  T, subtype(S; T), suptype(S; T), x. t(x), prop{i:l}
Lemmas	l member wf, fpf wf